Inference at * 
Iof proof for Lemma absval neg:


  i:{...0}. |i| = (-i) 

latex

 by InteriorProof ((((((((Unfold `absval` 0) 
CollapseTHEN (D 0))) 
CollapseTHENM (
CollapseTHENM (BoolCasesOnCExp 0 z i))) 
CollapseTHENM (AbReduce 0))) 
CollapseTHEN (
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok SupInf:t
CollapseTHEN () inil_term))) 

latex

C.

Definitions	True, ff, if b then t else f fi , , tt, t  T, x:A. B(x), {...i}
Lemmas	int lower wf, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf